package org.barad.architecture.analyzer.model.impl;

import java.util.Arrays;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;

import kodkod.ast.Formula;
import kodkod.ast.IntConstant;
import kodkod.ast.IntExpression;
import kodkod.ast.Relation;
import kodkod.ast.Variable;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.satlab.SATFactory;
import kodkod.instance.Bounds;
import kodkod.instance.Tuple;
import kodkod.instance.TupleFactory;
import kodkod.instance.TupleSet;
import kodkod.instance.Universe;

import org.apache.log4j.Logger;
import org.barad.architecture.analyzer.archpad.component.ArchPadComponent;
import org.barad.architecture.analyzer.model.component.Connector;
import org.barad.architecture.analyzer.model.component.Data;
import org.barad.architecture.analyzer.model.component.Processing;

import sun.security.smartcardio.SunPCSC.Factory;


//TODO: Add contraint that a component does not have the same
//dependency/service twice
@SuppressWarnings("unused")
public class CurrentModel extends SoftwareArchitectureModelBase {
	private Logger log;
	private static int indexOfDataComponents = 0;
	private static int indexOfProcessingComponents = 0;
	private static int indexOfConnectorComponents = 0;
	private TupleFactory tupleFactory;
	private Bounds bounds;
	
	/*
	 * //name of a component
	 * sig Name {}
	 */
	private Relation name = Relation.unary("Name");
	private Set<String> nameAtomSet = new HashSet<String>();

	/*
	 * //constraint
	 * sig Constraint{}
	 */
	private Relation constraint = Relation.unary("Constraint");
	private Set<String> constraintAtomSet = new HashSet<String>();

	/*
	 * //specification for dependencies/services
	 * sig Specification {
	 * input: set Constraint,
	 * output: set Constraint,
	 * general: set Constraint 
	 * }
	 */
	private Relation specification = Relation.unary("Specification");
	private Set<String> specificationAtomSet = new HashSet<String>();
	private Relation input = Relation.binary("Input");
	private Map<String, Set<String>> inputTupleSet = new HashMap<String, Set<String>>();
	private Relation output = Relation.binary("Output");
	private Map<String, Set<String>> outputTupleSet = new HashMap<String, Set<String>>();
	private Relation general = Relation.binary("General");
	private Map<String, Set<String>> generalTupleSet = new HashMap<String, Set<String>>();

	/*
	 * //all constraints are in the specification
	 * fact AllConstrainsInSpecification {
	 * Constraint in Specification.input + Specification.output + Specification.general
	 * }
	 */
	public Formula AllConstrainsInSpecification() {
		Variable c = Variable.unary("c");
		return c.in(specification.join(input)
				.union(specification.join(output))
				.union(specification.join(general)))
				.forAll(c.oneOf(constraint));
	}

	/*
	 * //should give a counterexample - OK (see below)
	 * assert TestAllConstrainsInSpecification {
	 * some c: Constraint | not c in Specification.input & Specification.output & Specification.general
	 * }
	 */
	public Formula TestAllConstrainsInSpecification() {
		Variable c = Variable.unary("c");
		return c.in(specification.join(input)
				.intersection(specification.join(output))
				.intersection(specification.join(general)))
				.not().forSome(c.oneOf(constraint));
	}

	/*
	 * Test if AllConstrainsInSpecification is valid - should find a counterexample -OK
	 */
	public Formula VerifyAllConstrainsInSpecification() {
		return AllConstrainsInSpecification().and(TestAllConstrainsInSpecification());
	}

	/*
	 * //architectural element
	 * abstract sig ArchitecturalElement {
	 * name:  one Name,
	 * services: set Specification, //ServiceSpecification,
	 * dependencies: set Specification, //DependencySpecification, 
	 * neighbour: set ArchitecturalElement
	 * } 
	 */
	private Relation architecturalElement = Relation.unary("ArchitecturalElement");
	private Set<String> architecturalElementAtomSet = new HashSet<String>();
	private Relation architecturalElementName = Relation.binary("ArchitecturalElementName");
	private Map<String, String> architecturalElementNameTupleSet = new HashMap<String, String>();
	private Relation service = Relation.binary("Service");
	private Map<String, Set<String>> serviceTupleSet = new HashMap<String, Set<String>>();
	private Relation dependency = Relation.binary("Dependency");
	private Map<String, Set<String>> dependencyTupleSet = new HashMap<String, Set<String>>();
	private Relation neighbor = Relation.binary("Neighbor");
	private Map<String, Set<String>> neighborTupleSet = new HashMap<String, Set<String>>();

	/*
	 * //processing element
	 * sig Processing extends ArchitecturalElement {}
	 */
	private Relation processing = Relation.unary("Processing");
	private Set<String> processingAtomSet = new HashSet<String>();

	/*
	 * //data element
	 * sig Data extends ArchitecturalElement {}
	 */
	private Relation data = Relation.unary("Data");
	private Set<String> dataAtomSet = new HashSet<String>();

	/*
	 * //connector element
	 * sig Connector extends ArchitecturalElement {}
	 */
	private Relation connector = Relation.unary("Connector");
	private Set<String> connectorAtomSet = new HashSet<String>();
	
	/*
	 * //no common entities
	 * fact NoCommonEntities {
	 * //no common names
	 * name in ArchitecturalElement one -> one Name
	 * //no common services specifications
	 * services in ArchitecturalElement one -> set Specification
	 * //no common dependencies specifications
	 * dependencies in ArchitecturalElement one -> set Specification
	 * }
	 */
	public Formula NoCommonEntities() {
		return noCommonNames().and(noCommonServices()).and(noCommonDependencies());
	}
	
	/* 
	 * //no common names
	 * name in ArchitecturalElement one -> one Name
	 */
	public Formula noCommonNames() {
		Variable ae1 = Variable.unary("ae1");
		Variable ae2 = Variable.unary("ae2");		
		Formula noCommonNames = (ae1.join(architecturalElementName).intersection(ae2.join(architecturalElementName)).some()
								.and(ae1.intersection(ae2).no())).not()
								.forAll(ae1.oneOf(architecturalElement))
								.forAll(ae2.oneOf(architecturalElement));
		System.out.println(noCommonNames.toString());
		return noCommonNames;
	}
	
	/*
	 * //no common services specifications
	 * services in ArchitecturalElement one -> set Specification
	 */
	public Formula noCommonServices() {
		Variable ae1 = Variable.unary("ae1");
		Variable ae2 = Variable.unary("ae2");		
		Formula noCommonServices = (ae1.join(service).intersection(ae2.join(service)).some()
								.and(ae1.intersection(ae2).no())).not()
								.forAll(ae1.oneOf(architecturalElement))
								.forAll(ae2.oneOf(architecturalElement));
		System.out.println(noCommonServices.toString());
		return noCommonServices;
	}
	
	/*
	 * //no common dependencies specifications
	 * dependencies in ArchitecturalElement one -> set Specification
	 */
	public Formula noCommonDependencies() {
		Variable ae1 = Variable.unary("ae1");
		Variable ae2 = Variable.unary("ae2");		
		Formula noCommonDependencies = (ae1.join(dependency).intersection(ae2.join(dependency)).some()
								.and(ae1.intersection(ae2).no())).not()
								.forAll(ae1.oneOf(architecturalElement))
								.forAll(ae2.oneOf(architecturalElement));
		System.out.println(noCommonDependencies.toString());
		return noCommonDependencies;
	}
	
	public void addDataComponent(Data data) {
		//add data atom
		String dataAtom = "Data" + indexOfDataComponents++;
		dataAtomSet.add(dataAtom);
		architecturalElementAtomSet.add(dataAtom);
		//add name atom
		nameAtomSet.add(data.getName());
		//add name tuple
		architecturalElementNameTupleSet.put(dataAtom, data.getName());
		//add service specifications tuples
		addSpecifications(dataAtom, data.getServices(), serviceTupleSet);
		//add dependency specifications tuples
		addSpecifications(dataAtom, data.getDependencies(), dependencyTupleSet); 
	}
	
	public void addProcessingComponent(Processing processing) {
		//add processing atom
		String processingAtom = "Processing" + indexOfProcessingComponents++;
		processingAtomSet.add(processingAtom);
		architecturalElementAtomSet.add(processingAtom);
		//add name atom
		nameAtomSet.add(processing.getName());
		//add name tuple
		architecturalElementNameTupleSet.put(processingAtom, processing.getName());
		//add service specifications tuples
		addSpecifications(processingAtom, processing.getServices(), serviceTupleSet);
		//add dependency specifications tuples
		addSpecifications(processingAtom, processing.getDependencies(), dependencyTupleSet); 
	}
	
	public void addConnectorComponent(Connector connector) {
		//add connector atom
		String connectorAtom = "Connector" + indexOfConnectorComponents++;
		connectorAtomSet.add(connectorAtom);
		architecturalElementAtomSet.add(connectorAtom);
		//add name atom
		nameAtomSet.add(connector.getName());
		//add name tuple
		architecturalElementNameTupleSet.put(connectorAtom, connector.getName());
		//add service specifications tuples 
		addSpecifications(connectorAtom, connector.getServices(), serviceTupleSet);
		//add dependency specifications tuples
		addSpecifications(connectorAtom, connector.getDependencies(), dependencyTupleSet); 
	}
	
	public Bounds getBounds() {
		return bounds;
	}
	
	/**
	 * TODO: Write me
	 * @param specifications
	 * @param tupleSet
	 * @param componentAtom
	 */
	private void addSpecifications(String componentAtom, List<Specification> specifications, Map<String, Set<String>> tupleSet) {
		for (Specification specification: specifications) {
			String specificationAtom = specification.getName();
			specificationAtomSet.add(specificationAtom);
			Set<String> specificationAtoms = tupleSet.get(componentAtom);
			if (specificationAtoms == null) {
				specificationAtoms = new HashSet<String>();
				tupleSet.put(componentAtom, specificationAtoms);
			}
			specificationAtoms.add(specificationAtom);
		}
	}
	
	private void initializeUniverse() {
		Universe universe = new Universe(aggregateUniverseAtoms());
		bounds = new Bounds(universe);
		tupleFactory = universe.factory();
		//add data tuples to the data realtion
		TupleSet dataTuples = createArityOneTuples(dataAtomSet);
		bounds.boundExactly(data, dataTuples);
		//add processing tuples to the processing realtion
		TupleSet processingTuples = createArityOneTuples(processingAtomSet);
		bounds.boundExactly(processing, processingTuples);
		//add connector tuples to the connector realtion
		TupleSet connectorTuples = createArityOneTuples(connectorAtomSet);
		bounds.boundExactly(connector, connectorTuples);
		//add architecturalElement tuples to architecturalElement relation
		TupleSet architecturalElementTuples = createArityOneTuples(architecturalElementAtomSet);
		bounds.boundExactly(architecturalElement, architecturalElementTuples);
		//add name tuples to the name relation
		TupleSet nameTuples = createArityOneTuples(nameAtomSet);
		bounds.boundExactly(name, nameTuples);
		//add specification tuples to the specification relation
		TupleSet specificationTuples = createArityOneTuples(specificationAtomSet);
		bounds.boundExactly(specification, specificationTuples);
		//add name tuples to the name relation
		TupleSet tuples = tupleFactory.noneOf(2);
		for (Map.Entry<String, String> tuple: architecturalElementNameTupleSet.entrySet()) {
			tuples.add(tupleFactory.tuple(tuple.getKey(), tuple.getValue()));
		}
		bounds.boundExactly(architecturalElementName, tuples);
		//add service tuples to the service relation
		TupleSet serviceTuples = createArityTwoTuples(serviceTupleSet);
		bounds.boundExactly(service, serviceTuples);
		//add dependency tuples to the dependency relation
		TupleSet dependencyTuples = createArityTwoTuples(dependencyTupleSet);
		bounds.boundExactly(dependency, dependencyTuples);
	}
	
	private TupleSet createArityTwoTuples(Map<String, Set<String>> tupleSet) {
		TupleSet tuples = tupleFactory.noneOf(2);
		for (Map.Entry<String, Set<String>> tuple: tupleSet.entrySet()) {
			for (String atom: tuple.getValue()) {
				tuples.add(tupleFactory.tuple(tuple.getKey(), atom));
			}
		}
		return tuples;
	}
	
	private TupleSet createArityOneTuples(Set<String> tupleSet) {
		TupleSet tuples = tupleFactory.noneOf(1);
		for (String tuple: tupleSet) {
			tuples.add(tupleFactory.tuple(tuple));
		}
		return tuples;
	}
	
	private Collection<String> aggregateUniverseAtoms() {
		Collection<String> universeAtoms = new LinkedList<String>();
		universeAtoms.addAll(nameAtomSet);
		universeAtoms.addAll(dataAtomSet);
		universeAtoms.addAll(connectorAtomSet);
		universeAtoms.addAll(processingAtomSet);
		universeAtoms.addAll(specificationAtomSet);
		universeAtoms.addAll(constraintAtomSet);
		//universeAtoms.addAll(architecturalElementAtomSet);
		return universeAtoms;
	}

	//run the model
	public static void main(String[] args) {
		//initialize model
		CurrentModel model = new CurrentModel();
		setUp(model);
		//initialize the solver
		Solver solver = new Solver();
		solver.options().setSolver(SATFactory.LightSAT4J);
		//all names must be unique
		Solution solution = solver.solve(model.NoCommonEntities(), model.getBounds());
		System.out.println(solution);
	}
	
	private static void setUp(CurrentModel model) {
		//ADD COMPONENTS TO THE MODEL
		//add a data component
		Data data = new Data();
		data.setName("Data");
		data.getServices().add(new Specification("ServiceSpecification1"));
		data.getServices().add(new Specification("ServiceSpecification2"));
		data.getDependencies().add(new Specification("DependencySpecification1"));
		data.getDependencies().add(new Specification("DependencySpecification2"));
		model.addDataComponent(data);
		//add a processing component
		Processing processing = new Processing();
		processing.setName("Connector");
		processing.getServices().add(new Specification("ServiceSpecification3"));
		processing.getServices().add(new Specification("ServiceSpecification4"));
		processing.getDependencies().add(new Specification("DependencySpecification3"));
		processing.getDependencies().add(new Specification("DependencySpecification4"));
		model.addProcessingComponent(processing);
		//add a connector component
		Connector connector = new Connector();
		connector.setName("Processing");
		connector.getServices().add(new Specification("ServiceSpecification5"));
		connector.getServices().add(new Specification("ServiceSpecification6"));
		connector.getDependencies().add(new Specification("DependencySpecification5"));
		connector.getDependencies().add(new Specification("DependencySpecification6"));
		model.addConnectorComponent(connector);
		//INITIALIZE THE UNIVERSE
		model.initializeUniverse();
	}
}
